HkdfSalt.lean🔗

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

HKDF Salt Type

Trusted: definitions used by the statement. Leaf definition of CryptoGames.HKDF.Salt, an optional 32-byte HKDF salt (none = no salt) shared between CryptoGames/AEAD/HKDFDefs.lean and LibsignalSpqr.lean without pulling CryptoGames / VCVio into the symbolic statement closure.

@[expose] public section

namespace CryptoGames

namespace HKDF

abbrev SaltL27–28 ↗#

A 32-byte HKDF salt (spqr message key); none = no salt.

abbrev Salt := Option (List.Vector (BitVec 8) 32)

end HKDF

end CryptoGames