Trusted in part. The theorems of Computational/Theorems/ use only the following definitions from this file (see Computational/docs/TRUSTED_BASE.md):

• The SPQR interface: the structure SpqrModel and its fields send, recv, sendPanics, recvPanics (the PQXDH-mode and SPQR V1 theorems).

• Concrete hooks and a helper: pubFromSecretHook, diffieHellmanHook, zeroizeSecretHook, readVec32 (rows of the CLI's hook table cliHookTablePlaced, SignalSession/CliRun.lean, which the statements about the CLI's ELF use). Everything else here, the layered program tripleRatchetProg / tripleRatchetExterns, entryOf and rngFillHook included, is checked by Lean.

This file states what the compiled AArch64 code of libsignal's triple ratchet (the Double Ratchet combined with the post-quantum SPQR ratchet) does, in terms of the pure session model (LibsignalBinary/Specifications/CryptoGames/Ratchet/LibsignalSession.lean). It defines the session program tripleRatchetProg (a loaded session image img with the base hooks sessionExterns plus the triple-ratchet hooks), the contracts of the callees it does not verify, the Hoare specs of the two entry points below and of the inlined try_decrypt_from_record region. The run statements (...RunStmt) the proofs establish are proof-side, in LibsignalBinary/Proofs/SpecLemmas/LibsignalTripleRatchetProofDefs.lean. Memory layouts and constants are in LibsignalBinary/Specifications/LibsignalTripleRatchetRepr.lean; the image guards are in LibsignalBinary/Specifications/LibsignalTripleRatchetGuards.lean.

Glossary: ABI = application binary interface; SS = SessionStructure; OTR = OutgoingTripleRatchet; SPE = SignalProtocolError; sret = the caller-provided structure-return buffer (here x0 for the two HookRng-generic entry points, x8 otherwise); SPQR / spqr = the Sparse Post-Quantum Ratchet; ML-KEM-768 = Module-Lattice-Based Key-Encapsulation Mechanism (ML-KEM-768); RNG = random number generator; UUID = universally unique identifier; ZST = zero-sized type; tape = the deterministic byte stream HookRng draws from (libsignal_session_rng_fill, DEV-E8); abs = the abstract hooks (any functions meeting the contracts of TripleRatchetHooks); IK = identity key; C = the session model's cryptographic primitives (Crypto: SHA-256 (Secure Hash Algorithm 256-bit) compression F, AES-256-CBC (Advanced Encryption Standard with 256-bit keys in Cipher Block Chaining mode) block cipher E / D, X25519 (Curve25519 elliptic-curve Diffie-Hellman) X, and public-key derivation pubKey); A = the Rust allocator model (RustAlloc); ghost = the logical (proof-only) parameters a spec is stated over; HMAC = Hash-based Message Authentication Code; HKDF = HMAC-based Key Derivation Function.

The specs of OutgoingTripleRatchet::from_session_state, ::apply_to_session_state and <SignalMessage as TryFrom<&[u8]>>::try_from (otrFromSpec, otrApplySpec, tryFromSpec) are proof-side, in LibsignalBinary/Proofs/SpecLemmas/LibsignalTripleRatchetProofDefs.lean.

In addition, recordDecryptSpec is a region contract for try_decrypt_from_record, which is inlined into session_message_decrypt_signal (model SessionState.tryDecryptFromRecord).

• everything in LibsignalSession.sessionExterns: SHA-256 compression, memcpy / memmove / memset, the no-alloc shim, black_box, Vec::remove::assert_failed, the allocator;

• concrete hooks: X25519 diffie_hellman = C.X and PublicKey::from(&StaticSecret) = C.pubKey, the two secret drops = zeroize, libsignal_session_rng_fill = the deterministic tape (DEV-E8);

• abstract hooks (abs, contracts in TripleRatchetHooks): the allocator (AllocHooks A, and __rust_alloc_zeroed from the same A, rustAllocZeroedSpec), AES-256-CBC encrypt / decrypt (named hypotheses matching the byte-level aesCbcEncrypt / aesCbcDecrypt functions), alloc::fmt::format_inner and core::fmt::write into a String (contracted to produce some owned String, since only error texts depend on them);

• no hook (reaching them halts, which every spec forbids, so the proofs must show they are not reached): __aarch64_ldadd8_rel / _relax, __aarch64_cas8_acq_rel, log::Log::log (logging off: logOff);

• the in-image spqr::send::<HookRng> and spqr::recv are not verified on non-empty post-quantum states: the general encrypt / decrypt statements take the named hypotheses SpqrSendOk / SpqrRecvOk, subroutine_ok statements in terms of SpqrModel.send / SpqrModel.recv (panics: SpqrModel.sendPanics / recvPanics), stated for the given abs. On a non-empty state their closures reach libcrux ML-KEM-768 / HMAC stubs with no contract here (lists at SpqrSendOk / SpqrRecvOk). On an empty state they reach none of them, so the proofs establish the empty-state instances without the hypotheses (proof-side statements in LibsignalBinary/Proofs/SpecLemmas/LibsignalTripleRatchetProofDefs.lean);

• the Rust panic entry points = Rust.withPanics; every other stub = abs (no contract: a proof can only cross it through SpqrSendOk / SpqrRecvOk).

libsignal-core, bytes, uuid, prost and spqr are whole crates in the image, so their functions are in-image code that the proofs execute, not hooks: in particular <PublicKey as TryFrom<&[u8]>>::try_from, PrivateKey::serialize, <ProtocolAddress as Display>::fmt (which calls core::fmt::write), ServiceId::parse_from_service_id_string (which calls Uuid::try_parse), bytes::panic_advance, Uuid::try_parse, prost's decode_varint_slow and DecodeError::from / push, spqr::decode_state and spqr::recv (guard inImageCallees_code).

Local IK ≠ remote IK (DEV-LS28: else upstream's self_session is true and max_forward_jumps differs from the model's); logging off; addresses parsed by serviceIdParse uuidParse (the specs are generic in the UUID parser; the statements instantiate them at the uuid 1.26.1 model uuidTryParse, which the in-image Uuid::try_parse computes). Sizes: plaintexts < 2^32, the parsed buffer < 2^32, message byte strings < 2^40 (signalMessageAt), decrypt: fewer than 2^32 receiver chains. Decrypt only (DEV-LS9): every stored skipped-key seed is 32 bytes (SeedsLen32), as libsignal itself always stores them.

• tripleRatchetExterns / tripleRatchetProg: the hook table and the program (image + hooks + panics) every statement runs.

• diffieHellmanHook, pubFromSecretHook, zeroizeSecretHook, rngFillHook: the concrete hooks (X25519, public-key derivation, secret zeroization, the RNG tape).

• aesEncSpec / aesDecSpec, formatInnerSpec, fmtWriteSpec, rustAllocZeroedSpec, collected in TripleRatchetHooks: the contracts assumed of the abstract hooks.

• SpqrModel: the abstract SPQR functions on serialized bytes; spqrSendSpec / spqrRecvSpec: the contracts of the in-image spqr::send / spqr::recv; SpqrSendOk / SpqrRecvOk: the named hypotheses that they meet them.

• SeedsLen32: the decrypt precondition that stored skipped-key seeds are 32 bytes (DEV-LS9).

• tryDecryptSpec, otrEncryptSpec: the binding specs of the two entry points (each with its ghost structure and .model).

• region_ok and recordDecryptSpec: the region-triple judgment and the region contract of the inlined try_decrypt_from_record.

• tripleRatchetExterns_abs (kernel-checked guard): the abstract hook names reach abs unchanged.