LibsignalAesCbc.lean🔗

Tier 2 · definitions used by the computational proof and symbolic proof 5 headline theorems depend on it 5 of 74 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.

Little-endian byte encodings and the return helper (toLEBytes, returnToLinkRegister)

Trusted: definitions used by the statement. The theorems of the default library (Computational/Theorems/ outside CliElfLib) use toLEBytes, blockToBytes, bytesToKey from this file; the theorems of Computational/Theorems/Main.lean (CliElfLib) also use returnToLinkRegister. Read them. The theorems here are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

This file defines the little-endian conversions between BitVecs (AES blocks and keys from LibsignalBinary/Specifications/CryptoGames/AEAD/CBCDefs.lean) and byte lists, as AArch64 loads and stores them, together with returnToLinkRegister, the return to the caller that the binary specifications' extern hooks end with. keyToBytes and the memcpy / memset hooks, used only by proofs, are in LibsignalBinary/Proofs/AesCbc/LibsignalAesCbcProofDefs.lean.

Glossary: AAPCS64 = the Arm 64-bit calling convention (arguments in x0–x7, result in x0, return address in lr); LE = little-endian.

returnToLinkRegister returns to lr and leaves every other register unchanged (the caller keeps nothing live in caller-saved registers across hook calls).

Despite the file and namespace name, nothing here specifies AES-CBC itself: the cryptographic primitives' machine code is hooked, not verified (DEV-E8).

Main definitions

toLEBytes: the low n bytes of a BitVec, least significant first.
blockToBytes: the 16 LE bytes of an AES Block.
bytesToKey: the 256-bit AesKey whose LE bytes are the given list.
returnToLinkRegister: return to the caller (pc := lr).

@[expose] public section

namespace CryptoVerification

namespace LibsignalAesCbc

open Arm64 ProofLib CryptoGames CryptoGames.CBC

Byte encodings (little-endian, as AArch64 loads and stores)

def toLEBytesL57–59 ↗#

The n LE bytes of x: byte j is bits 8j .. 8j+7.

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

2 declarations not shown (lines 61–66): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalAesCbc.blockToBytes, CryptoVerification.LibsignalAesCbc.bytesToKey

Extern hooks

def returnToLinkRegisterL70–71 ↗#

Return to the caller: pc := lr.

def returnToLinkRegister (s : State) : State := s.setPC (s.readReg64 .lr)

end LibsignalAesCbc

end CryptoVerification