ImageSymbols.lean🔗

Tier 2 · definitions used by the symbolic proof 4 headline theorems depend on it 22 of 69 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.

Declarations on this page (14)

External Stub Symbols and Wire Constants

ELF symbol names for hooked cryptographic primitives in signal-session and wire-framing tag and length constants.

@[expose] public section

namespace DY.Libsignal.Refinement

abbrev StubSymbolL23 ↗#

abbrev StubSymbol := String

abbrev sha256CompressSymbolL25–26 ↗#

Single-block SHA-256 compression [state, block] ↦ state' (sha2::sha256::compress256).

abbrev sha256CompressSymbol : StubSymbol := "sha2::sha256::compress256"

abbrev aesCbcEncryptSymbolL28–29 ↗#

AES-256-CBC encryption with PKCS#7 padding [plaintext, key, iv] ↦ ciphertext.

abbrev aesCbcEncryptSymbol : StubSymbol := "signal_crypto::aes_cbc::aes_256_cbc_encrypt"

abbrev aesCbcDecryptSymbolL31–32 ↗#

AES-256-CBC decryption with PKCS#7 unpadding [ciphertext, key, iv] ↦ Option plaintext.

abbrev aesCbcDecryptSymbol : StubSymbol := "signal_crypto::aes_cbc::aes_256_cbc_decrypt"

abbrev x25519AgreementSymbolL34 ↗#

abbrev x25519AgreementSymbol : StubSymbol := "<x25519_dalek::x25519::StaticSecret>::diffie_hellman"

abbrev x25519PublicKeySymbolL36–37 ↗#

abbrev x25519PublicKeySymbol : StubSymbol :=
  "<x25519_dalek::x25519::PublicKey as core::convert::From<&x25519_dalek::x25519::StaticSecret>>::from"

end DY.Libsignal.Refinement

namespace DY.Libsignal.PQXDH.Refinement

open DY.Libsignal.Refinement (StubSymbol)

abbrev libcruxHmacSymbolL45 ↗#

abbrev libcruxHmacSymbol : StubSymbol := "libcrux_hmac::hmac"

abbrev kyberEncapsSymbolL47 ↗#

abbrev kyberEncapsSymbol : StubSymbol := "libcrux_ml_kem::mlkem1024::kyber::encapsulate"

abbrev kyberDecapsSymbolL49 ↗#

abbrev kyberDecapsSymbol : StubSymbol := "libcrux_ml_kem::mlkem1024::kyber::decapsulate"

abbrev toEdwardsSymbolL51 ↗#

abbrev toEdwardsSymbol : StubSymbol := "<curve25519_dalek::montgomery::MontgomeryPoint>::to_edwards"

abbrev torsionFreeSymbolL53–54 ↗#

abbrev torsionFreeSymbol : StubSymbol :=
  "<curve25519_dalek::edwards::EdwardsPoint>::is_torsion_free"

abbrev wirePrekeyTagL56–57 ↗#

Leading wire tag byte for PreKeySignalMessage.

abbrev wirePrekeyTag : BitVec 8 := 3#8

abbrev preKeyBundleByteLengthL59–60 ↗#

Byte length of the serialized PublicBundle blob read by session_initiate.

abbrev preKeyBundleByteLength : Nat := 1813

end DY.Libsignal.PQXDH.Refinement

namespace DY.Libsignal.TripleRatchet.Refinement

abbrev wireWhisperTagL66–67 ↗#

Leading wire tag byte for SignalMessage.

abbrev wireWhisperTag : BitVec 8 := 2#8

end DY.Libsignal.TripleRatchet.Refinement